EventsWithOrder
== E:Type
==  (eq:EqDecider(E)
==  pred?:(E(?E))
==  info:(E((:Id  Top) + (:(:IdLnk  E)  Top)))
==  (oaxioms:EOrderAxioms(E; pred?; info)
==  Top)) 

latex

---

clarification:

EOrder{i:l}
== E:Type{i}
==  (eq:EqDecider(E)
==  pred?:(E(E + Unit))
==  info:(E((:Id  Top) + (:(:IdLnk  E)  Top)))
==  (oaxioms:EOrderAxioms{i}(E;
==  (oaxioms:EOpred?;
==  (oaxioms:EOinfo)
==  Top)) 

latex

Definitions	Type, EqDecider(T), Unit, x:AB(x), left + right, Id, IdLnk, x:A  B(x), EOrderAxioms(E; pred?; info), Top
FDL editor aliases	EOrder